$\forall$${\it es}$:ES, ${\it e'}$, $e$:E, $i$:$\mathbb{N}$.
\\[0ex]($i$ $<$ $\parallel$[$e$, ${\it e'}$]$\parallel$)
\\[0ex]$\Rightarrow$ (firstn($i$;[$e$, ${\it e'}$]) = if ($i$ =$_{0}$ 0) then [] else [$e$, pred([$e$, ${\it e'}$][$i$])] fi  $\in$ (E List))